auto-task(BlochSphere): drop unused BargmannInvariant import - #1309
auto-task(BlochSphere): drop unused BargmannInvariant import#1309jstoobysmith wants to merge 1 commit into
Conversation
Co-authored-by: Claude <noreply@anthropic.com>
|
Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally. If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks. If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip. Important: If a reviewer adds an |
1 participant
Minimize imports of
QuantumInfo/States/Pure/BlochSphere.leanWhat changed
Removed one unused import from
QuantumInfo/States/Pure/BlochSphere.lean:public import QuantumInfo.States.Pure.BargmannInvariantThe file defines
BlochSphere,blochPoint,solidAngle, and thesupporting lemmas purely in terms of Mathlib's
EuclideanSpace,WithLp.equiv,Matrix.crossProduct(the⨯₃notation),dotProduct,and
Complex/RealAPI. It references no declaration fromQuantumInfo.States.Pure.BargmannInvariant(or its transitiveBraketcontent), so that import is dead weight.What was kept and why
Both remaining imports are used directly and are required for the build:
Mathlib.LinearAlgebra.CrossProduct— provides the⨯₃cross-productnotation used in
solidAngle. Removing it breaks parsing.Mathlib.Analysis.InnerProductSpace.PiL2— providesEuclideanSpace,WithLp.equiv,EuclideanSpace.dist_eq/norm_eq. Removing it makesEuclideanSpaceunknown.I verified each by removing it individually and confirming the build fails,
so no further import could be trimmed.
Downstream impact
None.
BlochSphere.leanhas no importers in the repository, so nodownstream file needed a compensating import.
Verification
lake build QuantumInfocompletes successfully (8636 jobs) with nosorry, no new axioms, and no new errors or warnings. Onlyimportlines were touched; no code, docstrings, or declarations were modified.